nLab precompact space

Redirected from "precompact spaces".
Precompact spaces

Precompact spaces

Idea

A precompact space is one whose completion is compact. This makes sense for Cauchy spaces, but not for topological spaces. In the context of uniform spaces, precompact spaces are totally bounded spaces.

Precompact subsets (using the induced uniformity?) are one of the useful types of subset of a locally convex topological vector space, particularly with regard to defining topologies on dual spaces.

Definitions

Let XX be (in the most general situation) a Cauchy space; this includes uniform convergence spaces, uniform spaces, topological groups, topological vector spaces, and metric spaces (among other things) as special cases.

The following definitions are all equivalent even in weak constructive foundations:

Definition

The space XX is precompact if its completion is compact.

Definition

The space XX is precompact if every proper filter on XX has a (proper) Cauchy refinement.

Definition

The space XX is precompact if every net in XX has a Cauchy subnet (under any definition of ‘subnet’).

We also have this subsidiary notion:

Definition

A subset of XX is precompact if it is precompact (or …) for the inherited structure.

Sequential precompactness

Definition

The space XX is sequentially precompact if every sequence in XX has a Cauchy subsequence.

Properties

Theorem

Assuming weak countable choice, every sequentially precompact Lawvere metric space is a precompact Lawvere metric space.

 Relation to totally bounded spaces

Theorem

Every precompact space is a totally bounded space.

Theorem

That every totally bounded uniform space is precompact is equivalent to the ultrafilter principle, because the generalised Cantor space 2 K2^K is complete and totally bounded for any cardinal number KK.

Theorem

Assuming excluded middle and dependent choice, every totally bounded metric space is precompact.

(I don't know to what extent DC and EM are actually relevant to any of this; my reference HAF tacitly assumes them most of the time.)

See also

Last revised on November 16, 2022 at 21:54:22. See the history of this page for a list of all contributions to it.